COMMENT ⊗   VALID 00007 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "lspmac.pub[lsp,clt]" source
C00006 00003	.hd206 Fall 1977
C00009 00004	#. We will say that a list u is "intermittently contained" in
C00013 00005	#. (10pts)  Let e be a LISP expression in internal notation.  %2usecadr e%1 is
C00015 00006	#. (10pts)  What is compexp[$$(CONS (CAR X) Y), 0, ((X.1)(Y.2))$] as compiled by
C00016 00007	#. (10pts)  Write an abstract evaluator for Boolean expressions using the
C00019 ENDMK
C⊗;
.require "lspmac.pub[lsp,clt]" source;
.LSPFONT 
.allops
.basicops 
.MACRO  hd206 (TERM) ⊂
.BEGIN    NOFILL  TURNON "←→"
←COMPUTER SCIENCE DEPARTMENT
←STANFORD UNIVERSITY
.SKIP  
CS206  ←COMPUTING WITH SYMBOLIC EXPRESSIONS  →TERM
.TURNOFF
.END ⊃
.
.itemmac
.PORTION MAINPORTION
.PAGE ← 1
.hd206 Fall 1977
.skip
.cb Solutions to Final Exam.
.skip


	This examination is open book and notes.
Write LISP functions as follows except where something else is
requested.  Either notation may be used.
When a requested proof requires induction, be sure and write down
the induction principle appealed to and the specific predicate to
which the induction is applied.  There are a total of 60pts possible, distributed
as indicated.

.item←0
#. %2rev x%1 is the "reverse" of the arbitrary S-expression ⊗x.  Thus
%2rev%1 (A.(B.C)) = ((C.B).A).  Note that ⊗rev applied to a list
does not give the usual reversal of the list.

        (5pts)a. Write a recursive definition of ⊗rev. 

	(5pts)b. Prove that ⊗rev is total.

	(5pts)c. Prove that ⊗rev satisfies %2∀x: rev rev x = x%1.

1a.	⊗⊗rev x ← qif qat x qthen x qelse rev qd x . rev qa x⊗

1b.	We prove ⊗rev is total by S-expression induction using the induction predicate

			⊗⊗qP[x] ≡ issexp rev x⊗

	In the case ⊗⊗qat x⊗, ⊗⊗rev_x_=_x⊗ and we know ⊗⊗issexp_x⊗.  In the case
⊗⊗¬qat x⊗, we have ⊗⊗rev_x_=_rev_qqd_x_._rev_qqa_x⊗.  By the induction hypothesis
both arguments to ⊗cons satisfy ⊗issexp and we are done.

1c.	We prove this using S-expression induction using the induction predicate

			⊗⊗qP[x] ≡ rev rev x = x⊗

	In the case ⊗⊗qat x⊗, ⊗⊗rev_rev_x_=_x⊗.  In the case ⊗⊗¬qat x⊗ we have
.begin nofill

		⊗⊗rev rev x = rev[rev qd x . rev qa x]⊗   ...by definition of ⊗rev  
			  ⊗⊗= [rev rev qa x] . [rev rev qd x]⊗  ...by 1b,definition and LISP axioms
			  ⊗⊗= qa x . qd x⊗   ...by induction hypothesis
			  ⊗⊗= x⊗
.end
.next page
#. We will say that a list ⊗u is "intermittently contained" in
a list ⊗v if the elements of ⊗u occur in ⊗v in the same order
as in ⊗u but possibly separated by other elements of ⊗v.  We write
%2u_≤≤_v%1 for this relation.  Thus we have  (A_C_E)_≤≤_(X_A_B_C_A_F_D_E_G).

	(5pts)a. Write a recursive definition of %2u ≤≤ v%1.

Assume, to make the problem easier, that your %2u ≤≤ v%1 is total, and
prove

	(5pts)b. %2∀u:u ≤≤ u%1.

	(5pts)c. %2∀u v w:(u ≤≤ v ∧ v ≤≤ w ⊃ u ≤≤ w)%1.
.begin nofill

2a.	⊗⊗u ≤≤ v ← qif qn u qthen $T  ⊗
			⊗⊗qelse qif qn v qthen qNIL ⊗
			⊗⊗qelse qif qa u = qa v qthen qd u ≤≤ qd v⊗
			⊗⊗qelse u ≤≤ qd ⊗
.end

2b.	This proved by list induction with ⊗⊗qP[u] = u ≤≤ u⊗.  If ⊗⊗qn u⊗ then
it is true by definition of ≤≤.  If ⊗⊗¬qn u⊗ then ⊗⊗u ≤≤ u ≡ qd u ≤≤ qd u⊗ which
is true by the induction hypothesis.

2c.	This is proved by list induction on ⊗w with ⊗⊗qP[w] ≡ ∀u v: [u ≤≤ v ∧ v ≤≤ w ⊃ u ≤≤ w]⊗
In the case ⊗⊗qn w⊗ if ⊗⊗u ≤≤ v ∧ v ≤≤ w⊗ then from the definition we have ⊗⊗qn v⊗ and
⊗⊗qn u⊗ and thus ⊗⊗u ≤≤ w⊗ as desired.  To do the induction step we will use a 
lemma: ⊗⊗∀u w: ¬qn w ∧ u ≤≤ qd w ⊃ u ≤≤ w⊗.
In the case ⊗⊗¬qn w⊗ we observe that if ⊗⊗qn u⊗
then the result is trivial, so we may assume that ⊗⊗¬qn u⊗ and therefore ⊗⊗¬qn v⊗.
There are two possibilities.  If ⊗⊗qa v ≠ qa w⊗ then ⊗⊗v ≤≤ qd w⊗ and 
by the induction hypothesis ⊗⊗u ≤≤ qd w⊗ so by the lemma we are done.
If ⊗⊗qa v = qa w⊗ then ⊗⊗qd v ≤≤ qd w⊗  and we have two
further cases.  If ⊗⊗qa u ≠ qa v⊗ then ⊗⊗u ≤≤ qd v⊗ and again by induction  and 
the lemma we are done.
Otherwise we have ⊗⊗qd u ≤≤ qd v⊗ so by induction ⊗⊗qd u ≤≤ qd w⊗.  But also we
know that ⊗⊗qa u = qa v = qa w⊗ so by definition of ≤≤ we are done.
The lemma can be proved by induction on ⊗⊗size_u_+_size_w⊗ using the predicate

⊗⊗⊗qP[n] = ∀u w: [size u + size w = n ⊃ [¬qn w ∧ u ≤≤ qd w ⊃ u ≤≤ w] ∧ [¬qn u ∧ u ≤≤ w ⊃ qd u ≤≤ w]]⊗

#. (10pts)  Let ⊗e be a LISP expression in internal notation.  %2usecadr e%1 is
equivalent to ⊗e except that subexpressions of the form (CAR_(CDR_%2e%1)) are
replaced by (CADR_%2e%1).  Thus

	%2usecadr%1 (CONS (CAR (CDR (FOO X))) Y) = (CONS (CADR (FOO X)) Y).

We assume ⊗e is an expression which can be ⊗⊗eval⊗ed and hence is either an
atom or a list consisting of an operator expression followed by its operands.
Thus
.begin nofill

	⊗⊗usecadr x ← qif qat x qthen x⊗
		⊗⊗qelse qif [qa x = $CAR ∧ ¬qat qad x ∧ qaad x = $$CDR$] qthen 
$CADR . mapcar[qdad x, $$USECADR$]⊗
		⊗⊗qelse usecadr qa x . mapcar[qd x, $$USECADR$]⊗
.end
.next page
#. (10pts)  What is ⊗⊗compexp[$$(CONS (CAR X) Y), 0, ((X.1)(Y.2))$]⊗ as compiled by
LCOM0 and LCOM4.
.begin nofill

LCOM0:      (MOVE 1 1 P) 
            (PUSH P 1) 
            (MOVE 1 0 P) 
            (SUB P (α% 0 0 1 1)) 
            (CALL 1 (QUOTE CAR)) 
            (PUSH P 1) 
            (MOVE 1 1 P) 
            (PUSH P 1) 
            (MOVE 1 -1 P) 
            (MOVE 2 0 P) 
            (SUB P (α% 0 0 2 2)) 
            (CALL 2 (QUOTE CONS)) 

LCOM4:      (HLRZ 1 @ 1 P) 
            (MOVE 2 2 P) 
            (CALL 2 (QUOTE CONS))
.end

#. (10pts)  Write an abstract evaluator for Boolean expressions using the
abstract syntactic functions

	a. %2isand e%1 meaning that ⊗e has principal connective "and".

	b. %2isor e%1 meaning that ⊗e has principal connective "or".

	c. %2isnot e%1 meaning that ⊗e has principal connective "not".

	d. In each of the three above cases, %2operands e%1 gives a list
of the operands of the expression.  If ⊗e satisfies %2isnot%1, there is
exactly one operand, but in the other cases there may be any number.  The
LISP functions and predicates qa, qd, qn are applicable to these lists.

	e. %2isvar e%1 means that ⊗e is a Boolean variable, and in this
case the predicate %2true(e,%Ax%1) is true if ⊗e is true in the
state %Ax%1.

	Write a recursive definition of the predicate %2istrue(e,%Ax%1)
whose value is true or false according to whether the Boolean expression
⊗e is true in the state %Ax%1.  Your program should
not look at more terms of "and"s and "or"s than necessary to
decide the truth value.
.begin nofill

	⊗⊗istrue[e,qr] ← ⊗
		⊗⊗qif isvar e qthen true[e,qr]⊗
		⊗⊗qelse qif isnot e qthen ¬istrue[qa operands e, qr]⊗
		⊗⊗qelse qif isand e qthen istand[operands e, qr]⊗
		⊗⊗qelse qif isor e qthen istor[operands e, qr]⊗

	⊗⊗istand[u, qr] ← qif qn u qthen $T qelse qif ¬istrue[qa u, qr] qthen $F qelse istand[qd u, qr]⊗

	⊗⊗istor[u, qr] ← qif qn u qthen $F qelse qif istrue[qa u, qr] qthen $T qelse istor[qd u, qr]⊗
.end